D:Dsys, i:Id, k:Knd. Feasible(D)  (d-decl(D;i)(k))  M(i).da(k) 

latex

Definitions	x:A. B(x), P  Q, t  T, Feasible(D), P & Q, A & B, Prop
Lemmas	d-decl-subtype, d-feasible wf, Knd wf, Id wf, dsys wf